﻿module CSModel
type Domain = Ds of Set<int> | Di  of Set<int>
let symbolSet a = Ds (Set a)
let intSet a = Di (Set a)
type Def = VarDef of string*Domain
type Val = ValS of int | ValI of int
let s=ValS -1 //reference to create symbols, e.g. s?red, s?blue, etc.
type Expr =
    | Eq of Expr*Expr
    | Neq of Expr*Expr
    | And of Expr seq
    | Or of Expr seq
    | Var of Def
    | Val of Val
    | Plus of Expr*Expr
    | Minus of Expr*Expr
    | Mult of Expr*Expr
    | Div of Expr*Expr
    | Not of Expr
    | Mod of Expr*Expr
    | Abs of Expr
    | Gt of Expr*Expr
    | Lt of Expr*Expr
    | Ge of Expr*Expr
    | Le of Expr*Expr
let (~&) (v:Def) = Var(v) 
type Def with
    static member (?) (this:Def,p:string) = Symbols.Default====p
let d=VarDef("dummy",Ds Set.empty)
type Val with
    static member (?) (this:Val, p:string) = Symbols.Default====p|>ValS
    static member (==) (this:Val, e:Expr) = Eq(Val(this),e)
    static member (/=) (this:Val, e:Expr) = Neq(Val(this),e)
    static member (+) (this:Val, e:Expr) = Plus(Val(this),e)
    static member (-) (this:Val, e:Expr) = Minus(Val(this),e)
    static member (*) (this:Val, e:Expr) = Mult(Val(this),e)
    static member (/) (this:Val, e:Expr) = Div(Val(this),e)
    static member (%) (this:Val, e:Expr) = Mod(Val(this),e)
    static member op_GreaterThanOrEqual (this:Val, e:Expr) = Ge(Val(this),e)
    static member op_LessThanOrEqual (this:Val, e:Expr)    = Le(Val(this),e)
    static member op_GreaterThan (this:Val, e:Expr) = Gt(Val(this),e)
    static member op_LessThan (this:Val, e:Expr)    = Lt(Val(this),e)
type Expr with
    static member (==) (e1:Expr, e2:Expr) = Eq(e1,e2)
    static member (==) (e1:Expr, v:Val) = Eq(e1,Val(v))
    static member (!=) (e1:Expr, e2:Expr) = Neq(e1,e2)
    static member (!=) (e1:Expr, v:Val) = Neq(e1,Val(v))
    static member (+) (e1:Expr, e2:Expr) = Plus(e1,e2)
    static member (+) (e1:Expr, v:Val) = Plus(e1,Val(v))
    static member (-) (e1:Expr, e2:Expr) = Minus(e1,e2)
    static member (-) (e1:Expr, v:Val) = Minus(e1,Val(v))
    static member (*) (e1:Expr, e2:Expr) = Mult(e1,e2)
    static member (*) (e1:Expr, v:Val) = Mult(e1,Val(v))
    static member (/) (e1:Expr, e2:Expr) = Div(e1,e2)
    static member (/) (e1:Expr, v:Val) = Div(e1,Val(v))
    static member (%) (e1:Expr, e2:Expr) = Mod(e1,e2)
    static member (%) (e1:Expr, v:Val) = Mod(e1,Val(v))
    static member op_GreaterThanOrEqual (e1:Expr, e2:Expr) = Ge(e1,e2)
    static member op_GreaterThanOrEqual (e1:Expr, v:Val)   = Ge(e1,Val(v))
    static member op_LessThanOrEqual (e1:Expr, e2:Expr)    = Le(e1,e2)
    static member op_LessThanOrEqual (e1:Expr, v:Val)      = Le(e1,Val(v))
    static member op_GreaterThan (e1:Expr, e2:Expr)        = Gt(e1,e2)
    static member op_GreaterThan (e1:Expr, v:Val)          = Gt(e1,Val(v))
    static member op_LessThan (e1:Expr, e2:Expr)           = Lt(e1,e2)
    static member op_LessThan (e1:Expr, v:Val)             = Lt(e1,Val(v))

type ConstraintSystem = ConstraintSystem of Def seq*Expr seq

module NumericLiteralI =  
    let inline FromZero() = ValI 0
    let inline FromOne() = ValI 1
    let inline FromInt32(i:int) = ValI i
